Inference at * 1 
Iof proof for Lemma uni sat imp in uni set:



1. T : Type
2. a : T
3. Q : T
4. Q(a)
5. a':T. Q(a')  (a' = a)
  a  {x:T| Q(x)  (y:T. Q(y)  (y = x))}  

latex

 by ((MemTypeCD) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 6. y : T
C1: 7. Q(y)
C1:   y = a
C.

Definitions

P  Q, t  T, P  Q, x:A. B(x), x(s),